\begin{tabbing}
$\forall$\=$T$:Type, $p$:FinProbSpace, $l$:IdLnk, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, $P$:(State(${\it ds}$)$\rightarrow\mathbb{B}$),\+
\\[0ex]$f$:(State(${\it ds}$)$\rightarrow$Outcome$\rightarrow$$T$).
\-\\[0ex]Normal($T$)
\\[0ex]$\Rightarrow$ Normal(${\it ds}$)
\\[0ex]$\Rightarrow$ R{-}Feasible(\=at src($l$):\+
\\[0ex]action a(m) 
\\[0ex]p\=recondition $P$\+
\\[0ex]sends [tg,$f$] on link $l$)
\-\-
\end{tabbing}